<html>
<head><meta charset="utf-8"><title>Comparing Rust and Ada · wg-formal-methods · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/index.html">wg-formal-methods</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html">Comparing Rust and Ada</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="231768167"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231768167" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231768167">(Mar 25 2021 at 09:18)</a>:</h4>
<p>We recently published a CACM article on Rust:<br>
<a href="https://cacm.acm.org/magazines/2021/4/251364-safe-systems-programming-in-rust/fulltext">https://cacm.acm.org/magazines/2021/4/251364-safe-systems-programming-in-rust/fulltext</a><br>
Now a question (more of a comment, really) has come up pointing out that "safe systems programming" is also very much in the domain of Ada. Does anyone here know a good comparison of Rust and Ada? It is my understanding that Ada itself has no notion of ownership/borrowing, so where Rust shines when verifying memory management, Ada provides little support. Is that correct? (It is then often pointed out that Ada programs often use way fewer pointers than C++ or Rust programs would, but still, in terms of comparing language capabilities that seems like an important point.) What about concurrency; I read that newer versions of Ada have built-in "parallel blocks" but what does the type-checker do to avoid data races?<br>
And then there is Ada/SPARK, but that is backed by a theorem prover, so at this point we'd have to compare with Prusti or so, right? (Of course SPARK is much more mature that what Rust has in this space.)<br>
I've been curious about this myself for quite some time, and sadly never had the chance of having a long conversation with an Ada expert to get to the bottom of this.</p>



<a name="231768953"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231768953" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231768953">(Mar 25 2021 at 09:25)</a>:</h4>
<blockquote>
<p>It is my understanding that Ada itself has no notion of ownership/borrowing, so where Rust shines when verifying memory management, Ada provides little support. Is that correct?</p>
</blockquote>
<p>As far as I know, Ada has raw pointers, but no notion of ownership. However, Ada/SPARK recently got support for Rust like references with (Prusti) pledges.</p>



<a name="231769486"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231769486" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231769486">(Mar 25 2021 at 09:30)</a>:</h4>
<p>Maybe, <span class="user-mention" data-user-id="312719">@Xavier Denis</span> knows more since Ada/SPARK is based on Why3?</p>



<a name="231769928"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231769928" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231769928">(Mar 25 2021 at 09:34)</a>:</h4>
<p>(We're already chatting with Xavier's advisor, Jacques-Henri, about this -- but I was hoping to get some input from the wider community here.^^)</p>



<a name="231773360"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231773360" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231773360">(Mar 25 2021 at 10:02)</a>:</h4>
<p><span class="user-mention silent" data-user-id="120791">RalfJ</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada/near/231769928">said</a>:</p>
<blockquote>
<p>(We're already chatting with Xavier's advisor, Jacques-Henri, about this -- but I was hoping to get some input from the wider community here.^^)</p>
</blockquote>
<p>I see. I also would be curious to learn more about Ada and SPARK <span aria-label="smiling face" class="emoji emoji-263a" role="img" title="smiling face">:smiling_face:</span>.</p>



<a name="231773673"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231773673" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231773673">(Mar 25 2021 at 10:04)</a>:</h4>
<p><span class="user-mention" data-user-id="120791">@RalfJ</span> that’s no longer true! SPARK just added mutable borrows</p>



<a name="231773726"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231773726" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231773726">(Mar 25 2021 at 10:04)</a>:</h4>
<p>are we comparing Rust with Ada or SPARK now? ;)</p>



<a name="231773765"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231773765" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231773765">(Mar 25 2021 at 10:05)</a>:</h4>
<p>those seem like two different questions, no?</p>



<a name="231773789"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231773789" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231773789">(Mar 25 2021 at 10:05)</a>:</h4>
<p>the comment on the CACM site only talks about Ada</p>



<a name="231773828"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231773828" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231773828">(Mar 25 2021 at 10:05)</a>:</h4>
<p>but "Ada/SPARK is taking inspiration from Rust features" is certainly going to be part of our answer :)</p>



<a name="231775210"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231775210" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231775210">(Mar 25 2021 at 10:16)</a>:</h4>
<p>So spark is a subset of Ada</p>



<a name="231775212"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231775212" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231775212">(Mar 25 2021 at 10:16)</a>:</h4>
<p>And supports borrows in the rust sense</p>



<a name="231775213"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231775213" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231775213">(Mar 25 2021 at 10:16)</a>:</h4>
<p>And can verify programs using those</p>



<a name="231775214"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231775214" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231775214">(Mar 25 2021 at 10:16)</a>:</h4>
<p>I actually have one of the spark devs right next to me right now</p>



<a name="231775514"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231775514" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231775514">(Mar 25 2021 at 10:19)</a>:</h4>
<p><span class="user-mention silent" data-user-id="120791">RalfJ</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada/near/231773765">said</a>:</p>
<blockquote>
<p>those seem like two different questions, no?</p>
</blockquote>
<p>I have an impression that SPARK has a strong influence on the development of Ada. For example, Ada 2012 got first-class support for functional specifications. Therefore, I would not be surprised if an upcoming version of Ada would also have support for borrowing. I would say that both projects have a lot to learn from each other.</p>



<a name="231776368"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231776368" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231776368">(Mar 25 2021 at 10:26)</a>:</h4>
<p><span class="user-mention" data-user-id="120791">@RalfJ</span> they actually use a translation quite similar to RustHorn / Creusot and allow “prophetic specifications” like in creusot</p>



<a name="231776371"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231776371" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231776371">(Mar 25 2021 at 10:26)</a>:</h4>
<p>The SPARK being a subset of Ada comment is from the mouth of a SPARK dev</p>



<a name="231776869"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231776869" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231776869">(Mar 25 2021 at 10:31)</a>:</h4>
<p><a href="https://docs.adacore.com/spark2014-docs/html/ug/en/source/access.html#borrowing">https://docs.adacore.com/spark2014-docs/html/ug/en/source/access.html#borrowing</a></p>



<a name="231781136"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231781136" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231781136">(Mar 25 2021 at 11:04)</a>:</h4>
<p><span class="user-mention silent" data-user-id="312719">Xavier Denis</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada/near/231776371">said</a>:</p>
<blockquote>
<p>The SPARK being a subset of Ada comment is from the mouth of a SPARK dev</p>
</blockquote>
<p>so it's a bit like misra-C vs C?</p>



<a name="231781341"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231781341" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231781341">(Mar 25 2021 at 11:06)</a>:</h4>
<p>OTOH it some regards it seems to be "more" than Ada, namely by adding some fancy type system features (including, recently, some inspired by Rust)</p>



<a name="231781392"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231781392" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231781392">(Mar 25 2021 at 11:07)</a>:</h4>
<p><span class="user-mention silent" data-user-id="312719">Xavier Denis</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada/near/231776869">said</a>:</p>
<blockquote>
<p><a href="https://docs.adacore.com/spark2014-docs/html/ug/en/source/access.html#borrowing">https://docs.adacore.com/spark2014-docs/html/ug/en/source/access.html#borrowing</a></p>
</blockquote>
<p>I see no lifetimes there, so can I assume this is still much less flexible than what the borrow checker can do? for example, could you write the typed safe-to-use API of Rust's <code>Vec</code>?</p>



<a name="231781567"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231781567" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231781567">(Mar 25 2021 at 11:08)</a>:</h4>
<p><span class="user-mention silent" data-user-id="312719">Xavier Denis</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada/near/231775214">said</a>:</p>
<blockquote>
<p>I actually have one of the spark devs right next to me right now</p>
</blockquote>
<p>ah that'd be great if they could comment on this. :D<br>
I am particularly wondering about concurrency -- do Ada or Ada+SPARK have mechanisms in place to ensure data-race freedom? Is there something equivalent to Rust's <code>Mutex</code>/<code>RwLock</code> that enables safe shared mutable state?</p>



<a name="231782655"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231782655" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231782655">(Mar 25 2021 at 11:17)</a>:</h4>
<p>Another aspect we're interested is formal proofs -- is there a formal model of Ada or SPARK with a proof of type safety, or anything like that?</p>



<a name="231785826"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231785826" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231785826">(Mar 25 2021 at 11:45)</a>:</h4>
<p>I told Yannick to sign up for Zulip so he should log on soon to give proper answers</p>



<a name="231786003"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231786003" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231786003">(Mar 25 2021 at 11:46)</a>:</h4>
<p>(Happy to use other communication channels as well, e.g. our MPI Mattermost or email or whatever)</p>



<a name="231786060"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231786060" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231786060">(Mar 25 2021 at 11:46)</a>:</h4>
<p>From my understanding of spark borrows they are much more “local” so they don’t need a complex borrow checker like rust</p>



<a name="231786078"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231786078" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231786078">(Mar 25 2021 at 11:46)</a>:</h4>
<p>I’m no Ada expert though</p>



<a name="231786273"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231786273" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231786273">(Mar 25 2021 at 11:48)</a>:</h4>
<p>And I believe they mean it’s a subset of Ada in the sense that a subset of Ada programs are valid spark</p>



<a name="231786337"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231786337" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231786337">(Mar 25 2021 at 11:48)</a>:</h4>
<p>So imposing additional data flow analyses is no issue for them</p>



<a name="231786457"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231786457" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231786457">(Mar 25 2021 at 11:49)</a>:</h4>
<p>right, but that still restricts what you can do in terms of abstraction</p>



<a name="231786530"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231786530" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231786530">(Mar 25 2021 at 11:50)</a>:</h4>
<p>Yes it’s not equivalent to Rust</p>



<a name="231786589"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231786589" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231786589">(Mar 25 2021 at 11:50)</a>:</h4>
<p>you could do a borrow-checker-like thing in C and carve out some appropriate "subset of C" that way, but where Rust shines is giving types to APIs that have interesting ownership patterns (such as <code>Vec</code>)</p>



<a name="231786591"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231786591" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231786591">(Mar 25 2021 at 11:50)</a>:</h4>
<p>Also afaik they have no formal proof of type system soundness</p>



<a name="231786618"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231786618" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231786618">(Mar 25 2021 at 11:51)</a>:</h4>
<p>and to get those types you need to add something (namely a more expressive type system), not just reject more programs</p>



<a name="231786686"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231786686" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231786686">(Mar 25 2021 at 11:51)</a>:</h4>
<p>Agreed, but different use cases I think</p>



<a name="231786808"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231786808" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231786808">(Mar 25 2021 at 11:52)</a>:</h4>
<p>I think Yannick will be best places to answer these questions</p>



<a name="231786871"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231786871" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231786871">(Mar 25 2021 at 11:53)</a>:</h4>
<p>I really only have a passing knowledge of SPARK, particularly in how they translate and reason on their borrows</p>



<a name="231803514"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231803514" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Yannick Moy <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231803514">(Mar 25 2021 at 13:52)</a>:</h4>
<p>Very nice article btw! I was invited by <span class="user-mention" data-user-id="312719">@Xavier Denis</span> to answer questions on Ada and SPARK. SPARK is indeed a subset of Ada, like MISRA C is a subset of C (I even wrote a comparison about that at <a href="https://learn.adacore.com/courses/SPARK_for_the_MISRA_C_Developer/">https://learn.adacore.com/courses/SPARK_for_the_MISRA_C_Developer/</a>), but the goal with SPARK is to provide guarantees statically about the program, by static analysis and proof. Ada does not provide as many guarantees statically as Rust regarding dynamic memory and concurrency. Regarding pointers, its main focus is on pointers to the stack, which by typing can't become dangling pointers: you can declare local pointer types for pointer variables that _can_ point to a stack variable of the same or a less-nested scope, but can't point to a stack variable of a more-nested scope. You can also have a form of local memory reclamation by declaring a local pointer type with its own "memory pool" in which all dynamically allocated pointers of that type are allocated, which is freed when the scope is exited. The typing rules ensure that this does not lead again to dangling pointers. But there are no guarantees for more liberal use of dynamic allocation, in particular the "free" function is called Unchecked_Deallocation and opens the door to double-free or use-after-free, and you are not protected against memory leaks when not using a local "memory pool".  Similarly, Ada does not provide as many guarantees statically as Rust regarding concurrent access to shared data/resources. The safe way to access shared data/resources is to use "protected objects" (with their own lock) but nothing forces you to comply with it. The parallel features in the upcoming version of Ada are not implemented in GNAT/SPARK today and may not be for some time. </p>
<p>SPARK supports both pointers and concurrency safely by restricting what you can do. For concurrency, that means only accessing shared data that is "synchronized" (exact definition here: <a href="https://docs.adacore.com/live/wave/spark2014/html/spark2014_rm/tasks-and-synchronization.html">https://docs.adacore.com/live/wave/spark2014/html/spark2014_rm/tasks-and-synchronization.html</a> so that includes atomic objects and protected objects). For pointers, that means following a simple ownership policy modeled after Rust ownership policy. That allows us to deal with pointers in proof like we do for other data structures, without worrying about possible aliasing. The difficulty comes with mutating a linked data structure while traversing it, and here my colleague Claire Dross initially implemented last year the pledges from Prusti and recently replaced them with the prophecy variables that <span class="user-mention" data-user-id="312719">@Xavier Denis</span> is using in his PhD work. You can see an example of use of prophecy variables here: <a href="https://github.com/yannickmoy/am2sp/blob/db487410991cd5373c56f0f251013b85c2e5aef0/src/list_arith.adb#L34">https://github.com/yannickmoy/am2sp/blob/db487410991cd5373c56f0f251013b85c2e5aef0/src/list_arith.adb#L34</a> and the equivalent with pledges here: <a href="https://github.com/yannickmoy/am2sp/blob/0ecdec063a5f09aa246061154c8a6b560d87b85a/src/list_arith.adb#L35">https://github.com/yannickmoy/am2sp/blob/0ecdec063a5f09aa246061154c8a6b560d87b85a/src/list_arith.adb#L35</a> The SPARK User's Guide now contains a variety of typical loop invariants with prophecy variables: <a href="https://docs.adacore.com/live/wave/spark2014/html/spark2014_ug/en/source/loop.html">https://docs.adacore.com/live/wave/spark2014/html/spark2014_ug/en/source/loop.html</a> (just look for occurrences of "At_End").   </p>
<p>That being said, we'd like to include more static guarantees in Ada itself in the future (enforced only by compilation, while the current solution for SPARK is based on a mix of ownership checking and proof for things like non-null pointer dereference checks and absence of memory leaks), and of course we're looking at Rust as a main source of inspiration here!</p>



<a name="231804098"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231804098" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Yannick Moy <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231804098">(Mar 25 2021 at 13:55)</a>:</h4>
<p>Also, regarding formalization, there is very little regarding how SPARK deals with pointers, published recently: <a href="https://hal.archives-ouvertes.fr/INRIA-SACLAY/hal-03094566v1">https://hal.archives-ouvertes.fr/INRIA-SACLAY/hal-03094566v1</a></p>



<a name="231808289"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Comparing%20Rust%20and%20Ada/near/231808289" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Comparing.20Rust.20and.20Ada.html#231808289">(Mar 25 2021 at 14:17)</a>:</h4>
<p><span class="user-mention" data-user-id="400488">@Yannick Moy</span> thanks a lot, that is very helpful :)</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>